| Definitions | s = t, ecl-trans-tuple{i:l}(ds; da), ecl-trans(x), normal-type{i:l}(T), mkid{$x:ut2}, False,  A, msg-spec-loc-decl(snd; i; da), update-spec-decl(upd; ds), EqDecider(T), isrcv(k), destination(l), lnk(k), fpf-dom(eq; x; f), Kind-deq, fpf-all(A; eq; f; x,v.P(x;v)), normal-da{i:l}(da), update-spec(ds; da), normal-ds{i:l}(ds), msg-spec(ds; da), fpf-cap(f; eq; x; z), id-deq, ecl(ds; da), msg-item(ds; da; k; l), t.1,  x.A(x), t.2, rec(x.A(x)), ma-valtype(da; k),  , atom{$n:n}, {x:A| B(x)} , ecl-machine{$ecl:ut2}(i; ds; da; A; snd; upd), es realizer ind,  x. t(x), es_realizer{i:l}, x,y,z,w. t(x;y;z;w), rationals, x,y,z,u,v,w. t(x;y;z;u;v;w), decl-type{i:l}(ds; x), x,y,z,w,v. t(x;y;z;w;v), fpf(A; a.B(a)), finite-prob-space,  , decl-state(ds), IdLnk, x,y,z. t(x;y;z), R-realizes{i:l}(R; es.P(es)), ecl-mng{i:l}(es; i; ds; da; x; snd; upd), R-consistent(R; es), event_system{i:l}, R-Feasible{i:l}(R), Rplus(left; right), ecl-machine3(ds; da; x; T; ks; a; snd), ecl-machine2(i; ds; da; x; T; ks; a; upd), ecl-machine1{$ecl:ut2}(i; ds; da; A), Id, [], cons(car; cdr), subtype(S; T), top, isect(A; x.B(x)), void, prop{i:l}, l_all(L; T; x.P(x)),  b, (x  l), Type,  T, True, <a, b>, ecl-kinds(x), x:A  B(x), ||as||, ge(i; j), P    Q, P  Q, x:A  B(x), left + right, sqequal(s; t), t T, sq_type(T),  x:A. B(x), P Q, guard(T), type List, Knd, ecl-trans-ks(v), spreadn(u; a,b,c,d,e,f,g.v(a;b;c;d;e;f;g)), es realizer ind Rplus compseq tag def, R-compat{i:l}(A; B), P Q, let x,y = A in B(x;y), ecl-trans-type(A), ecl-trans-a(v),  , A  B, suptype(S; T), ecl-mng-update{i:l}(es; i; ds; da; x; z; upd), update-spec-vars(upd), l-all(L; x.P(x)), ecl-mng-sends{i:l}(es; i; ds; da; x; l; snd), msg-spec-links(snd), source(l),  , A c B, l[i], #$n, a < b,  x:A. B(x), alle-at(es; i; e.P(e)), with decls ds dasends on l from e include f(e) and only these for tags in tgs, msg-spec-loc(snd; i), es-decls(es;i;ds;da), fpf-join(eq; f; g), fpf-single(x; v), es-vartype(es; i; x), idlnk-deq, ecl-tags(l; snd), deq-member(eq; x; L), loc(e), fpf-sub(A; a.B(a); eq; f; g), es-E(es), if b then t else f fi , f(a), ecl-m3(a; snd; x; l), rcv(l,tg), tagged-list-messages(s; v; L), mapfilter(f; P; L), es-kind(es; e), es-val(es; e), es-state-when(es; e), es-valtype(es; e), es-state(es; i), Unit,  b, P  Q, e' e.P(e'), fpf-ap(f; eq; x),  , @i discrete ds, es-isrcv(es; e), product-deq(A; B; a; b), es-bact{i:l}(ds; da; a; es; n; e1; e2), eq_id(a; b), es-rcvtype(es; e), es-acttype(es; e), locl(a), tt, ff, es-init(es;e), constant_function(f; A; B), qle(r; s), e < e', val-axiom(E;V;M;info;pred?;init;Trans;Choose;Send;val;time), Msg(M), kindcase(k; a.f(a); l,t.g(l;t)), EState(T), EOrderAxioms(E;pred?;info), decidable(P), case b of inl(x) => s(x) | inr(y) => t(y), let x = a in b(x), concat(ll), map(f; as), spreadn(a; x,y,z.t(x;y;z)), es-when(es; x; e), append(as; bs), filter(P; l), x(s), es-after(es; x; e), list_accum(x,a.f(x;a); y; l), bor(p; q), es-isconst(es; i; x), null(as), ecl ind eclbase compseq tag def, ecl ind eclseq compseq tag def, ecl ind ecland compseq tag def, ecl ind eclor compseq tag def, ecl ind eclrepeat compseq tag def, ecl ind eclact compseq tag def, ecl ind eclthrow compseq tag def, ecl ind eclcatch compseq tag def, rec-case(a) of [] => s | x::y => z.t(x;y;z), es-trans-state-from{i:l}(es;ks;g;z;e1;e2), es-hist{i:l}(es;e1;e2), es-info(es;e), x,y. t(x;y), es-le(es; e; e'), atom2-deq-aux, eq_atom{$n:n}(x; y) |
| Lemmas | nat sq, subtype-fpf-cap-void, iff wf, eq atom wf2, rev implies wf, atom2-deq-aux, es-le-loc, iff imp equal bool, list accum wf, es-interval-eq, es-le weakening eq, decidable false, le wf, append is nil, ecl wf, ecl-induction, null wf3, es-isconst wf, bor wf, assert of null, or functionality wrt iff, assert of bor, es-after wf, alle-at wf, ecl-mng-update wf, update-spec-vars wf, fpf-ap wf, filter is nil, l member subtype, false wf, fpf-cap-single1, bool sq, bool cases, fpf-join-cap-sq, member wf, deq wf, map wf, append wf, nat properties, subtype rel wf, es-when wf, fpf-sub weakening, fpf-sub-join-left2, decidable equal Id, es-loc-init, es-isrcv-loc, es-init wf, bfalse wf, btrue wf, locl wf, es-acttype wf, es-rcvtype wf, assert-eq-id, es-bact wf, mapfilter wf, subtype rel dep function, product-deq wf, es-isrcv wf, es-state-subtype, es-state-subtype2, bnot wf, assert-deq-member, not functionality wrt iff, assert of bnot, iff transitivity, eqff to assert, eqtt to assert, fpf-single wf, fpf-join wf, es-val wf, es-valtype wf, es-loc wf, es-state wf, tagged-list-messages wf, es-state-when wf, es-kind wf, es-E wf, rcv wf, ecl-m3 wf, deq-member wf, ifthenelse wf, ecl-tags wf, es-sends-iff functionality, Id sq, idlnk-deq wf, member-remove-repeats, es-vartype wf, es-decls-join-single, es-decls-iff, es-decls wf, msg-spec-loc-decl-implies, select wf, length wf1, ecl-mng-sends wf, msg-spec-links wf, l-all-iff, ecl-1-3-compat, R-compat wf, ecl-1-2-compat, subtype rel self, ecl-trans-a wf, ecl-trans-type wf, R-compat-Rplus2, ecl-2-3-compat, Knd sq, cons one one, non neg length, l member wf, top wf, length wf nat, ecl-machine3-realizes, es realizer wf, rationals wf, Id wf, Knd wf, IdLnk wf, decl-type wf, decl-state wf, fpf wf, bool wf, finite-prob-space wf, true wf, squash wf, es realizer ind wf, ecl-machine3 wf, ecl-machine2 wf, Rplus wf, ecl-machine1 wf, R-consistent wf, event system wf, ecl-machine2-realizes, ecl-trans-ks wf, ecl-trans-tuple wf, ecl-trans wf, ecl-kinds-ecl-trans, ecl-machine1-realizes, nat wf, ma-valtype wf, pi2 wf, pi1 wf, msg-item wf, id-deq wf, fpf-cap wf, normal-ds wf, normal-da wf, fpf-trivial-subtype-top, Kind-deq wf, fpf-dom wf, assert wf, lnk wf, ldst wf, isrcv wf, ecl-kinds wf, l all wf2, update-spec-decl wf, msg-spec-loc-decl wf, not wf |
upd:update-spec(ds; da).